package at.ptasat.solver.thread;

import java.io.File;
import java.io.FileInputStream;
import java.io.IOException;
import java.io.OutputStream;
import java.io.PrintStream;

import at.tasat.Configuration;
import at.tasat.cnf.Cnf;
import at.tasat.io.OutputFormatter;
import at.tasat.parser.DimacsParser;
import at.tasat.solver.Solver;
import at.ptasat.solver.AsyncSolver;
import at.ptasat.solver.AsyncSolverListener;

public class AsyncThreadSolver extends AsyncSolver {
	private static Object globalMutex = new Object();
	private static File currentCnfFile = null;
	private static Cnf currentCnf = null;
	private Object localMutex = new Object();
	private Thread thread;
	private boolean isSolving = false;
	private boolean isKilled = false;

	public AsyncThreadSolver(int id, AsyncSolverListener callback, OutputStream out, OutputStream err, String arguments) {
		super(id, callback, out, err, arguments);
	}

	@Override
	public void start(String additionalArguments, File file) throws Exception {
		synchronized (globalMutex) {
			if (isKilled) {
				return;
			}
			String arguments = additionalArguments + " " + getArguments() + " " + file.getAbsolutePath();
			final Configuration config = Configuration.get(arguments.split(" "));
			final Cnf cnf = getCnf(file);			
			synchronized (localMutex) {
				isSolving = true;
				thread = new Thread() {
					@Override
					public void run() {
						runWorker(config, cnf);
					}
				};
				thread.start();
			}
			
		}
	}

	private void runWorker(Configuration config, Cnf cnf) {
		Solver solver = null;
		try {
			solver = Solver.create(config.getSolverConfig(), cnf);
			boolean sat = solver.solve();
			(new PrintStream(getOut())).println(OutputFormatter.getResultString(sat, solver.getAssignment().getAllAssignments()));

			synchronized (localMutex) {
				isSolving = false;
			}
			fireSolved();
		} catch (InterruptedException e) {
		} catch (Throwable e) {
			if (e.getCause() instanceof ThreadDeath) {
				return;
			}
			(new PrintStream(getErr())).println(OutputFormatter.getErrorString(e));
		} finally {
			synchronized (localMutex) {
				isSolving = false;
			}
			if (solver != null) {
				solver.releaseThreadManager();
			}
		}
	}

	private static Cnf getCnf(File file) throws IOException {
		if (currentCnfFile == null) {
			currentCnfFile = file;
			FileInputStream fileInputStream = new FileInputStream(file);
			currentCnf = DimacsParser.parse(fileInputStream);
			fileInputStream.close();
		} else if (currentCnfFile != file) {
			throw new IllegalArgumentException("expected same file as in last call");
		}
		return currentCnf;
	}

	@Override
	public void kill() {
		synchronized (localMutex) {
			isKilled = true;
			if (thread != null && isSolving) {
				thread.interrupt();
			}
		}
		synchronized (globalMutex) {
			currentCnfFile = null;
			currentCnf = null;
		}
	}

}
